i, j:. (i <z j ~ tt)  (i < j) 

latex

Up	sqequal 1, sqequal 1
Definitions	t  T, x:A. B(x), P  Q, , P & Q, P  Q
Lemmas	int sq, btrue wf, assert of lt int, eqtt to assert, assert wf, bool wf, iff transitivity